ecl{-}halt{-}type(${\it da}$;$x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case ecl{-}halt{-}kind($x$) of inl($k$) =$>$ Valtype(${\it da}$;$k$) $\mid$ inr($z$) =$>$ Top